The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^2)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

A(b(x1)) → b(a(B(A(x1))))
B(a(x1)) → a(b(A(B(x1))))
A(a(x1)) → x1
B(b(x1)) → x1

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

A(b(z0)) → b(a(B(A(z0))))
A(a(z0)) → z0
B(a(z0)) → a(b(A(B(z0))))
B(b(z0)) → z0

Tuples:

A'(b(z0)) → c(B'(A(z0)), A'(z0))
B'(a(z0)) → c2(A'(B(z0)), B'(z0))

S tuples:

A'(b(z0)) → c(B'(A(z0)), A'(z0))
B'(a(z0)) → c2(A'(B(z0)), B'(z0))

K tuples:none
Defined Rule Symbols:

A, B

Defined Pair Symbols:

A', B'

Compound Symbols:

c, c2

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace A'(b(z0)) → c(B'(A(z0)), A'(z0)) by

A'(b(b(z0))) → c(B'(b(a(B(A(z0))))), A'(b(z0)))
A'(b(a(z0))) → c(B'(z0), A'(a(z0)))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

A(b(z0)) → b(a(B(A(z0))))
A(a(z0)) → z0
B(a(z0)) → a(b(A(B(z0))))
B(b(z0)) → z0

Tuples:

B'(a(z0)) → c2(A'(B(z0)), B'(z0))
A'(b(b(z0))) → c(B'(b(a(B(A(z0))))), A'(b(z0)))
A'(b(a(z0))) → c(B'(z0), A'(a(z0)))

S tuples:

B'(a(z0)) → c2(A'(B(z0)), B'(z0))
A'(b(b(z0))) → c(B'(b(a(B(A(z0))))), A'(b(z0)))
A'(b(a(z0))) → c(B'(z0), A'(a(z0)))

K tuples:none
Defined Rule Symbols:

A, B

Defined Pair Symbols:

B', A'

Compound Symbols:

c2, c

(5) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

A(b(z0)) → b(a(B(A(z0))))
A(a(z0)) → z0
B(a(z0)) → a(b(A(B(z0))))
B(b(z0)) → z0

Tuples:

B'(a(z0)) → c2(A'(B(z0)), B'(z0))
A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))

S tuples:

B'(a(z0)) → c2(A'(B(z0)), B'(z0))
A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))

K tuples:none
Defined Rule Symbols:

A, B

Defined Pair Symbols:

B', A'

Compound Symbols:

c2, c

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace B'(a(z0)) → c2(A'(B(z0)), B'(z0)) by

B'(a(a(z0))) → c2(A'(a(b(A(B(z0))))), B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0), B'(b(z0)))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

A(b(z0)) → b(a(B(A(z0))))
A(a(z0)) → z0
B(a(z0)) → a(b(A(B(z0))))
B(b(z0)) → z0

Tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(A'(a(b(A(B(z0))))), B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0), B'(b(z0)))

S tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(A'(a(b(A(B(z0))))), B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0), B'(b(z0)))

K tuples:none
Defined Rule Symbols:

A, B

Defined Pair Symbols:

A', B'

Compound Symbols:

c, c2

(9) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

A(b(z0)) → b(a(B(A(z0))))
A(a(z0)) → z0
B(a(z0)) → a(b(A(B(z0))))
B(b(z0)) → z0

Tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

S tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

K tuples:none
Defined Rule Symbols:

A, B

Defined Pair Symbols:

A', B'

Compound Symbols:

c, c2

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

A'(b(b(z0))) → c(A'(b(z0)))

We considered the (Usable) Rules:none
And the Tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(A'(x₁)) = [2] + [3]x₁ + [2]x₁²   
POL(B'(x₁)) = [1] + [2]x₁²   
POL(a(x₁)) = x₁   
POL(b(x₁)) = [2] + x₁   
POL(c(x₁)) = x₁   
POL(c2(x₁)) = x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

A(b(z0)) → b(a(B(A(z0))))
A(a(z0)) → z0
B(a(z0)) → a(b(A(B(z0))))
B(b(z0)) → z0

Tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

S tuples:

A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

K tuples:

A'(b(b(z0))) → c(A'(b(z0)))

Defined Rule Symbols:

A, B

Defined Pair Symbols:

A', B'

Compound Symbols:

c, c2

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

We considered the (Usable) Rules:none
And the Tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(A'(x₁)) = [2] + [4]x₁   
POL(B'(x₁)) = [4] + [4]x₁   
POL(a(x₁)) = [2] + x₁   
POL(b(x₁)) = [5] + x₁   
POL(c(x₁)) = x₁   
POL(c2(x₁)) = x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

A(b(z0)) → b(a(B(A(z0))))
A(a(z0)) → z0
B(a(z0)) → a(b(A(B(z0))))
B(b(z0)) → z0

Tuples:

A'(b(b(z0))) → c(A'(b(z0)))
A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

S tuples:

A'(b(a(z0))) → c(B'(z0))

K tuples:

A'(b(b(z0))) → c(A'(b(z0)))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

Defined Rule Symbols:

A, B

Defined Pair Symbols:

A', B'

Compound Symbols:

c, c2

(15) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

A'(b(a(z0))) → c(B'(z0))
B'(a(a(z0))) → c2(B'(a(z0)))
B'(a(b(z0))) → c2(A'(z0))

Now S is empty

(16) BOUNDS(O(1), O(1))